1  /-
  2  Copyright (c) 2019 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl
  5  
  6  Hahn decomposition theorem
  7  
  8  TODO:
  9  * introduce finite measures (into nnreal)
 10  * show general for signed measures (into ℝ)
 11  -/
 12  import measure_theory.measure_space
src         └──────────────────────────┘
 13  
 14  open set lattice filter
 15  open_locale classical topological_space
 16  
 17  namespace measure_theory
 18  
 19  variables {α : Type*} [measurable_space α] {μ ν : measure α}
 20  
 21  -- suddenly this is necessary?!
 22  private lemma aux {m : ℕ} {γ d : ℝ} (h : γ - (1 / 2) ^ m < d) :
 23    γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d :=
 24  by linarith
src     └────────
typ     └────────
doc     └────────
txt     └────────
par     └────────
pid             
 25  
src  
typ  
doc  
txt  
par  
pid  
 26  lemma hahn_decomposition (hμ : μ univ < ⊤) (hν : ν univ < ⊤) :
 27    ∃s, is_measurable s ∧
 28      (∀t, is_measurable t → t ⊆ s → ν t ≤ μ t) ∧
 29      (∀t, is_measurable t → t ⊆ - s → μ t ≤ ν t) :=
 30  begin
 31    let d : set α → ℝ := λs, ((μ s).to_nnreal : ℝ) - (ν s).to_nnreal,
src    └──────┘      └──┘ └─┘    └────────────┘ └┘    └─────────┘
typ    └──────┘      └──┘ └─┘    └────────────┘ └┘    └─────────┘
doc    └──────┘      └──┘ └─┘    └────────────┘ └┘    └─────────┘
txt    └──────┘      └──┘ └─┘    └────────────┘ └┘    └─────────┘
par    └──────┘      └──┘ └─┘    └────────────┘ └┘    └─────────┘
pid    └───┘└─┘      └──┘ └─┘    └────────────┘ └┘    └────────┘
 32    let c : set ℝ := d '' {s | is_measurable s },
src    └──────┘    └──┘    └──┘              └┘
typ    └──────┘    └──┘    └──┘              └┘
doc    └──────┘    └──┘    └──┘              └┘
txt    └──────┘    └──┘    └──┘              └┘
par    └──────┘    └──┘    └──┘              └┘
pid    └───┘└─┘    └──┘    └──┘              └┘
 33    let γ : ℝ := Sup c,
src    └──────┘ └──┘   
typ    └──────┘ └──┘   
doc    └──────┘ └──┘   
txt    └──────┘ └──┘   
par    └──────┘ └──┘   
pid    └───┘└─┘ └──┘   
 34  
 35    have hμ : ∀s, μ s < ⊤ := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hμ,
src    └────────┘      └──┘      └──┘                                       └──┘
typ    └────────┘      └──┘      └──┘                                       └──┘
doc    └────────┘      └──┘      └──┘                                       └──┘
txt    └────────┘      └──┘      └──┘                                       └──┘
par    └────────┘      └──┘      └──┘                                       └──┘
pid    └─────┘└─┘      └──┘      └──┘                                       └──┘
 36    have hν : ∀s, ν s < ⊤ := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hν,
id                                       └────────────┘  └──────────┘   └─────────┘    └┘
src    └────────┘      └──┘      └──┘└────────────┘ └──────────┘ └─────────┘└──┘
typ    └────────┘     └──┘      └──┘└────────────┘ └──────────┘ └─────────┘└──┘└┘
doc    └────────┘      └──┘      └──┘                                       └──┘
txt    └────────┘      └──┘      └──┘                                       └──┘
par    └────────┘      └──┘      └──┘                                       └──┘
pid    └─────┘└─┘      └──┘      └──┘                                       └──┘
st    └──────────────────────────────────────────────────────────────────────────────────┘└─
 37    have to_nnreal_μ : ∀s, ((μ s).to_nnreal : ennreal) = μ s :=
id                                               └─────┘   
src    └─────────────────┘      └────────────┘└─────┘└┘  └───
typ    └─────────────────┘      └────────────┘└─────┘└┘ └───
doc    └─────────────────┘      └────────────┘└─────┘└┘   └───
txt    └─────────────────┘      └────────────┘       └┘   └───
par    └─────────────────┘      └────────────┘       └┘   └───
pid    └──────────────┘└─┘      └────────────┘       └┘   └───
st   ──────────────────────────────────────────────────────────────
 38      (assume s, ennreal.coe_to_nnreal $ ne_top_of_lt $ hμ _),
id                  └───────────────────┘   └──────────┘   └┘
src  ───┘       └──┘└───────────────────┘ └──────────┘   └─┘
typ  ───┘       └──┘└───────────────────┘ └──────────┘ └┘└─┘
doc  ───┘       └──┘                                     └─┘
txt  ───┘       └──┘                                     └─┘
par  ───┘       └──┘                                     └─┘
pid  ───┘       └──┘                                     └─┘
st   ──────────────────────────────────────────────────────────┘└─
 39    have to_nnreal_ν : ∀s, ((ν s).to_nnreal : ennreal) = ν s :=
id                                               └─────┘    
src    └─────────────────┘      └────────────┘└─────┘└┘   └───
typ    └─────────────────┘      └────────────┘└─────┘└┘  └───
doc    └─────────────────┘      └────────────┘└─────┘└┘   └───
txt    └─────────────────┘      └────────────┘       └┘   └───
par    └─────────────────┘      └────────────┘       └┘   └───
pid    └──────────────┘└─┘      └────────────┘       └┘   └───
st   ──────────────────────────────────────────────────────────────
 40      (assume s, ennreal.coe_to_nnreal $ ne_top_of_lt $ hν _),
id                  └───────────────────┘   └──────────┘   └┘
src  ───┘       └──┘└───────────────────┘ └──────────┘   └─┘
typ  ───┘       └──┘└───────────────────┘ └──────────┘ └┘└─┘
doc  ───┘       └──┘                                     └─┘
txt  ───┘       └──┘                                     └─┘
par  ───┘       └──┘                                     └─┘
pid  ───┘       └──┘                                     └─┘
st   ──────────────────────────────────────────────────────────┘└─
 41  
st   
 42    have d_empty : d ∅ = 0, { simp [d], rw [measure_empty, measure_empty], simp },
id                                          └───────────┘  └───────────┘
src    └─────────────┘  └┘    └────┘   └──┘└───────────┘└┘└───────────┘  └───┘
typ    └─────────────┘ └┘    └────┘  └──┘└───────────┘└┘└───────────┘  └───┘
doc    └─────────────┘   └┘    └────┘   └──┘             └┘               └───┘
txt    └─────────────┘   └┘    └────┘   └──┘             └┘               └───┘
par    └─────────────┘   └┘    └────┘   └──┘             └┘               └───┘
pid    └──────────┘└─┘                └┘             └┘                   
st   ───────────────────────┘└──┘└──────┘└─────────────────┘└─────────────┘└──────┘└┘
 43  
st   
 44    have d_split : ∀s t, is_measurable s → is_measurable t →
id                          └───────────┘     └───────────┘
src    └─────────────┘ └─┘                └───────────┘  
typ    └─────────────┘ └─┘ └───────────┘  └───────────┘  
doc    └─────────────┘ └─┘                └───────────┘  
txt    └─────────────┘ └─┘                               
par    └─────────────┘ └─┘                               
pid    └──────────┘└─┘ └─┘                               
st   ───────────────────────────────────────────────────────────
 45      d s = d (s \ t) + d (s ∩ t),
id                           
src  ───┘       └┘    
typ  ───┘       └┘   
doc  ───┘        └┘      
txt  ───┘        └┘      
par  ───┘        └┘      
pid  ───┘        └┘      
st   ──────────────────────────────┘└─
 46    { assume s t hs ht,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid      └──────────────┘
st   ───┘└──────────────┘└─
 47      simp only [d],
id                  
src      └─────────┘ 
typ      └─────────┘
doc      └─────────┘ 
txt      └─────────┘ 
par      └─────────┘ 
pid          └──┘└┘ 
st   ────────────────┘└─
 48      rw [measure_eq_inter_diff hs ht, measure_eq_inter_diff hs ht,
id           └───────────────────┘ └┘ └┘  └───────────────────┘ └┘ └┘
src      └──┘└───────────────────┘    └┘└───────────────────┘    └─
typ      └──┘└───────────────────┘└┘└┘└┘└───────────────────┘└┘└┘└─
doc      └──┘                         └┘                         └─
txt      └──┘                         └┘                         └─
par      └──┘                         └┘                         └─
pid        └┘                         └┘                         └─
st   ──────────────────────────────────┘└───────────────────────────┘└─
 49        ennreal.to_nnreal_add (hμ _) (hμ _), ennreal.to_nnreal_add (hν _) (hν _),
id         └───────────────────┘         └┘     └───────────────────┘         └┘
src  ─────┘└───────────────────┘   └──┘   └───┘└───────────────────┘   └──┘   └────
typ  ─────┘└───────────────────┘   └──┘ └┘└───┘└───────────────────┘   └──┘ └┘└────
doc  ─────┘                        └──┘   └───┘                        └──┘   └────
txt  ─────┘                        └──┘   └───┘                        └──┘   └────
par  ─────┘                        └──┘   └───┘                        └──┘   └────
pid  ─────┘                        └──┘   └───┘                        └──┘   └────
st   ────────────────────────────────────────┘└───────────────────────────────────┘└─
 50        nnreal.coe_add, nnreal.coe_add],
id         └────────────┘  └────────────┘
src  ─────┘└────────────┘└┘└────────────┘
typ  ─────┘└────────────┘└┘└────────────┘
doc  ─────┘              └┘              
txt  ─────┘              └┘              
par  ─────┘              └┘              
pid  ─────┘              └┘              
st   ───────────────────┘└──────────────┘└──
 51      simp only [sub_eq_add_neg, neg_add],
id                  └────────────┘  └─────┘
src      └─────────┘└────────────┘└┘└─────┘
typ      └─────────┘└────────────┘└┘└─────┘
doc      └─────────┘              └┘       
txt      └─────────┘              └┘       
par      └─────────┘              └┘       
pid          └──┘└┘              └┘       
st   ──────────────────────────────────────┘└─
 52      ac_refl },
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid             
st   ───────────┘└┘
 53  
st   
 54    have d_Union : ∀(s : ℕ → set α), (∀n, is_measurable (s n)) → monotone s →
id                             └─┘         └───────────┘          └──────┘
src    └─────────────┘ └───┘  └─┘     └───────────┘   └─┘ └──────┘  
typ    └─────────────┘ └───┘ └─┘    └───────────┘   └─┘ └──────┘  
doc    └─────────────┘ └───┘          └───────────┘   └─┘ └──────┘  
txt    └─────────────┘ └───┘                          └─┘           
par    └─────────────┘ └───┘                          └─┘           
pid    └──────────┘└─┘ └───┘                          └─┘           
st   ────────────────────────────────────────────────────────────────────────────
 55      tendsto (λn, d (s n)) at_top (𝓝 (d (⋃n, s n))),
id       └─────┘               └────┘       
src  ───┘└─────┘  └─┘    └─┘└────┘      └─┘
typ  ───┘└─────┘  └─┘    └─┘└────┘     └─┘
doc  ───┘└─────┘  └─┘    └─┘└────┘      └─┘
txt  ───┘         └─┘    └─┘               └─┘
par  ───┘         └─┘    └─┘               └─┘
pid  ───┘         └─┘    └─┘               └─┘
st   ─────────────────────────────────────────────────┘└─
 56    { assume s hs hm,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid      └────────────┘
st   ───┘└────────────┘└─
 57      refine tendsto.sub _ _;
id              └─────────┘
src      └─────┘└─────────┘└──┘
typ      └─────┘└─────────┘└──┘
doc      └─────┘           └──┘
txt      └─────┘           └──┘
par      └─────┘           └──┘
pid                       └──┘
st   ────────────────────────────
 58        refine (nnreal.tendsto_coe.2 $
id                 └────────────────┘
src        └─────┘ └────────────────┘└─┘ 
typ        └─────┘ └────────────────┘└─┘ 
doc        └─────┘                   └─┘ 
txt        └─────┘                   └─┘ 
par        └─────┘                   └─┘ 
pid                                 └─┘ 
st   ─────────────────────────────────────
 59          (ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ ⊤ _).comp $ tendsto_measure_Union hs hm),
id            └───────────────────────┘    └──────────┘                   └───────────────────┘ └┘ └┘
src  ───────┘ └───────────────────────┘  └──────────┘└─────┘ └───────┘ └───────────────────┘    
typ  ───────┘ └───────────────────────┘  └──────────┘└─────┘ └───────┘ └───────────────────┘└┘└┘
doc  ───────┘                                        └─────┘ └───────┘                          
txt  ───────┘                                        └─────┘ └───────┘                          
par  ───────┘                                        └─────┘ └───────┘                          
pid  ───────┘                                        └─────┘ └───────┘                          
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
 60      exact hμ _,
id             └┘
src      └────┘  └┘
typ      └────┘└┘└┘
doc      └────┘  └┘
txt      └────┘  └┘
par      └────┘  └┘
pid             └┘
st   ─────────────┘└─
 61      exact hν _ },
id             └┘
src      └────┘  └─┘
typ      └────┘└┘└─┘
doc      └────┘  └─┘
txt      └────┘  └─┘
par      └────┘  └─┘
pid             └┘
st   ──────────────┘└┘
 62  
st   
 63    have d_Inter : ∀(s : ℕ → set α), (∀n, is_measurable (s n)) → (∀n m, n ≤ m → s m ⊆ s n) →
id                              └─┘         └───────────┘                            
src    └─────────────┘ └───┘  └─┘     └───────────┘   └─┘   └─┘        └┘ 
typ    └─────────────┘ └───┘  └─┘    └───────────┘   └─┘   └─┘        └┘ 
doc    └─────────────┘ └───┘          └───────────┘   └─┘   └─┘          └┘ 
txt    └─────────────┘ └───┘                          └─┘   └─┘          └┘ 
par    └─────────────┘ └───┘                          └─┘   └─┘          └┘ 
pid    └──────────┘└─┘ └───┘                          └─┘   └─┘          └┘ 
st   ───────────────────────────────────────────────────────────────────────────────────────────
 64      tendsto (λn, d (s n)) at_top (𝓝 (d (⋂n, s n))),
id       └─────┘               └────┘        
src  ───┘└─────┘  └─┘    └─┘└────┘       └─┘
typ  ───┘└─────┘  └─┘    └─┘└────┘      └─┘
doc  ───┘└─────┘  └─┘    └─┘└────┘       └─┘
txt  ───┘         └─┘    └─┘               └─┘
par  ───┘         └─┘    └─┘               └─┘
pid  ───┘         └─┘    └─┘               └─┘
st   ─────────────────────────────────────────────────┘└─
 65    { assume s hs hm,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid      └────────────┘
st   ───┘└────────────┘└─
 66      refine tendsto.sub _ _;
id              └─────────┘
src      └─────┘└─────────┘└──┘
typ      └─────┘└─────────┘└──┘
doc      └─────┘           └──┘
txt      └─────┘           └──┘
par      └─────┘           └──┘
pid                       └──┘
st   ────────────────────────────
 67        refine (nnreal.tendsto_coe.2 $
id                 └────────────────┘
src        └─────┘ └────────────────┘└─┘ 
typ        └─────┘ └────────────────┘└─┘ 
doc        └─────┘                   └─┘ 
txt        └─────┘                   └─┘ 
par        └─────┘                   └─┘ 
pid                                 └─┘ 
st   ─────────────────────────────────────
 68          (ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ ⊤ _).comp $ tendsto_measure_Inter hs hm _),
id            └───────────────────────┘    └──────────┘                   └───────────────────┘ └┘ └┘
src  ───────┘ └───────────────────────┘  └──────────┘└─────┘ └───────┘ └───────────────────┘    └─┘
typ  ───────┘ └───────────────────────┘  └──────────┘└─────┘ └───────┘ └───────────────────┘└┘└┘└─┘
doc  ───────┘                                        └─────┘ └───────┘                          └─┘
txt  ───────┘                                        └─────┘ └───────┘                          └─┘
par  ───────┘                                        └─────┘ └───────┘                          └─┘
pid  ───────┘                                        └─────┘ └───────┘                          └─┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────────┘└─
 69      exact hμ _,
id             └┘
src      └────┘  └┘
typ      └────┘└┘└┘
doc      └────┘  └┘
txt      └────┘  └┘
par      └────┘  └┘
pid             └┘
st   ─────────────┘└─
 70      exact ⟨0, hμ _⟩,
id                 └┘
src      └────┘ └─┘  └─┘
typ      └────┘ └─┘└┘└─┘
doc      └────┘ └─┘  └─┘
txt      └────┘ └─┘  └─┘
par      └────┘ └─┘  └─┘
pid            └─┘  └─┘
st   ──────────────────┘└─
 71      exact hν _,
id             └┘
src      └────┘  └┘
typ      └────┘└┘└┘
doc      └────┘  └┘
txt      └────┘  └┘
par      └────┘  └┘
pid             └┘
st   ─────────────┘└─
 72      exact ⟨0, hν _⟩ },
id                 └┘
src      └────┘ └─┘  └──┘
typ      └────┘ └─┘└┘└──┘
doc      └────┘ └─┘  └──┘
txt      └────┘ └─┘  └──┘
par      └────┘ └─┘  └──┘
pid            └─┘  └─┘
st   ───────────────────┘└┘
 73  
st   
 74    have bdd_c : bdd_above c,
id                  └───────┘ 
src    └───────────┘└───────┘
typ    └───────────┘└───────┘
doc    └───────────┘└───────┘
txt    └───────────┘         
par    └───────────┘         
pid    └────────┘└─┘         
st   ─────────────────────────┘└─
 75    { use (μ univ).to_nnreal,
id             └──┘
src      └──┘  └──┘└─────────┘
typ      └──┘ └──┘└─────────┘
doc      └──┘      └─────────┘
txt      └──┘      └─────────┘
par      └──┘      └─────────┘
pid               └────────┘
st   ───┘└────────────────────┘└─
 76      rintros r ⟨s, hs, rfl⟩,
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid             └─────────────┘
st   ─────────────────────────┘└─
 77      refine le_trans (sub_le_self _ $ nnreal.coe_nonneg _) _,
id              └──────┘  └─────────┘     └───────────────┘
src      └─────┘└──────┘ └─────────┘└─┘ └───────────────┘└───┘
typ      └─────┘└──────┘ └─────────┘└─┘ └───────────────┘└───┘
doc      └─────┘                    └─┘                  └───┘
txt      └─────┘                    └─┘                  └───┘
par      └─────┘                    └─┘                  └───┘
pid                                └─┘                  └───┘
st   ──────────────────────────────────────────────────────────┘└─
 78      rw [nnreal.coe_le, ← ennreal.coe_le_coe, to_nnreal_μ, to_nnreal_μ],
id           └───────────┘    └────────────────┘  └─────────┘  └─────────┘
src      └──┘└───────────┘└──┘└────────────────┘└┘           └┘           
typ      └──┘└───────────┘└──┘└────────────────┘└┘└─────────┘└┘└─────────┘
doc      └──┘             └──┘                  └┘           └┘           
txt      └──┘             └──┘                  └┘           └┘           
par      └──┘             └──┘                  └┘           └┘           
pid        └┘             └──┘                  └┘           └┘           
st   ────────────────────┘└────────────────────┘└───────────┘└───────────┘└──
 79      exact measure_mono (subset_univ _) },
id             └──────────┘  └─────────┘
src      └────┘└──────────┘ └─────────┘└──┘
typ      └────┘└──────────┘ └─────────┘└──┘
doc      └────┘                        └──┘
txt      └────┘                        └──┘
par      └────┘                        └──┘
pid                                   └─┘
st   ──────────────────────────────────────┘└┘
 80  
st   
 81    have c_nonempty : c.nonempty := nonempty.image _ ⟨_, is_measurable.empty⟩,
id                       └────────┘    └────────────┘       └─────────────────┘
src    └────────────────┘└────────┘└──┘└────────────┘└─┘ └─┘└─────────────────┘
typ    └────────────────┘└────────┘└──┘└────────────┘└─┘ └─┘└─────────────────┘
doc    └────────────────┘└────────┘└──┘              └─┘ └─┘                   
txt    └────────────────┘          └──┘              └─┘ └─┘                   
par    └────────────────┘          └──┘              └─┘ └─┘                   
pid    └─────────────┘└─┘          └──┘              └─┘ └─┘                   
st   ──────────────────────────────────────────────────────────────────────────┘└─
 82  
st   
 83    have d_le_γ : ∀s, is_measurable s → d s ≤ γ := assume s hs, le_cSup bdd_c ⟨s, hs, rfl⟩,
id                       └───────────┘                           └─────┘ └───┘         └─┘
src    └────────────┘  └───────────┘      └──┘      └─────┘└─────┘       └┘  └┘└─┘
typ    └────────────┘  └───────────┘    └──┘      └─────┘└─────┘└───┘  └┘  └┘└─┘
doc    └────────────┘  └───────────┘      └──┘      └─────┘              └┘  └┘   
txt    └────────────┘                     └──┘      └─────┘              └┘  └┘   
par    └────────────┘                     └──┘      └─────┘              └┘  └┘   
pid    └─────────┘└─┘                     └──┘      └─────┘              └┘  └┘   
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
 84  
st   
 85    have : ∀n:ℕ, ∃s : set α, is_measurable s ∧ γ - (1/2)^n < d s,
id                      └─┘  └───────────┘                
src    └─────┘ └┘  └──┘└─┘ └───────────┘     └┘   
typ    └─────┘ └┘  └──┘└─┘└───────────┘    └┘  
doc    └─────┘ └┘   └──┘     └───────────┘      └┘    
txt    └─────┘ └┘   └──┘                        └┘    
par    └─────┘ └┘   └──┘                        └┘    
pid    └───┘└┘ └┘   └──┘                        └┘    
st   ─────────────────────────────────────────────────────────────┘└─
 86    { assume n,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
 87      have : γ - (1/2)^n < γ := sub_lt_self γ (pow_pos (half_pos zero_lt_one) n),
id                               └─────────┘   └─────┘  └──────┘ └─────────┘  
src      └─────┘    └┘    └──┘└─────────┘  └─────┘ └──────┘└─────────┘└┘ 
typ      └─────┘    └┘  └──┘└─────────┘ └─────┘ └──────┘└─────────┘└┘
doc      └─────┘    └┘    └──┘                                        └┘ 
txt      └─────┘    └┘    └──┘                                        └┘ 
par      └─────┘    └┘    └──┘                                        └┘ 
pid      └───┘└┘    └┘    └──┘                                        └┘ 
st   ─────────────────────────────────────────────────────────────────────────────┘└─
 88      rcases exists_lt_of_lt_cSup c_nonempty this with ⟨r, ⟨s, hs, rfl⟩, hlt⟩,
id              └──────────────────┘ └────────┘ └──┘
src      └─────┘└──────────────────┘              └──────────────────────────┘
typ      └─────┘└──────────────────┘└────────┘└──┘└──────────────────────────┘
doc      └─────┘└──────────────────┘              └──────────────────────────┘
txt      └─────┘                                  └──────────────────────────┘
par      └─────┘                                  └──────────────────────────┘
pid                                              └──────────────────────────┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
 89      exact ⟨s, hs, hlt⟩ },
id                └┘  └─┘
src      └────┘  └┘  └┘   └┘
typ      └────┘ └┘└┘└┘└─┘└┘
doc      └────┘  └┘  └┘   └┘
txt      └────┘  └┘  └┘   └┘
par      └────┘  └┘  └┘   └┘
pid             └┘  └┘   
st   ──────────────────────┘└┘
 90    rcases classical.axiom_of_choice this with ⟨e, he⟩,
id            └───────────────────────┘ └──┘
src    └─────┘└───────────────────────┘    └───────────┘
typ    └─────┘└───────────────────────┘└──┘└───────────┘
doc    └─────┘                             └───────────┘
txt    └─────┘                             └───────────┘
par    └─────┘                             └───────────┘
pid                                       └───────────┘
st   ───────────────────────────────────────────────────┘└─
 91    change ℕ → set α at e,
id                └─┘ 
src    └─────┘  └─┘ └───┘
typ    └─────┘  └─┘└───┘
doc    └─────┘      └───┘
txt    └─────┘      └───┘
par    └─────┘      └───┘
pid                └──┘
st   ──────────────────────┘└─
 92    have he₁ : ∀n, is_measurable (e n) := assume n, (he n).1,
id                    └───────────┘                    └┘
src    └─────────┘  └───────────┘   └───┘      └──┘    └─┘
typ    └─────────┘  └───────────┘  └───┘      └──┘ └┘ └─┘
doc    └─────────┘  └───────────┘   └───┘      └──┘    └─┘
txt    └─────────┘                  └───┘      └──┘    └─┘
par    └─────────┘                  └───┘      └──┘    └─┘
pid    └──────┘└─┘                  └──┘      └──┘    └┘
st   ─────────────────────────────────────────────────────────┘└─
 93    have he₂ : ∀n, γ - (1/2)^n < d (e n) := assume n, (he n).2,
id                                                     └┘
src    └─────────┘      └┘       └───┘      └──┘    └─┘
typ    └─────────┘     └┘     └───┘      └──┘ └┘ └─┘
doc    └─────────┘      └┘       └───┘      └──┘    └─┘
txt    └─────────┘      └┘       └───┘      └──┘    └─┘
par    └─────────┘      └┘       └───┘      └──┘    └─┘
pid    └──────┘└─┘      └┘       └──┘      └──┘    └┘
st   ───────────────────────────────────────────────────────────┘└─
 94  
st   
 95    let f : ℕ → ℕ → set α := λn m, (finset.Ico n (m + 1)).inf e,
id                     └─┘            └────────┘                
src    └──────┘    └─┘ └──┘ └───┘ └────────┘    └───────┘
typ    └──────┘    └─┘└──┘ └───┘ └────────┘    └───────┘
doc    └──────┘        └──┘ └───┘ └────────┘    └───────┘
txt    └──────┘        └──┘ └───┘               └───────┘
par    └──────┘        └──┘ └───┘               └───────┘
pid    └───┘└─┘        └──┘ └───┘               └───────┘
st   ────────────────────────────────────────────────────────────┘└─
 96  
st   
 97    have hf : ∀n m, is_measurable (f n m),
id                     └───────────┘  
src    └────────┘ └─┘ └───────────┘    
typ    └────────┘ └─┘ └───────────┘   
doc    └────────┘ └─┘ └───────────┘    
txt    └────────┘ └─┘                  
par    └────────┘ └─┘                  
pid    └─────┘└─┘ └─┘                  
st   ──────────────────────────────────────┘└─
 98    { assume n m,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid      └────────┘
st   ───┘└────────┘└─
 99      simp only [f, finset.inf_eq_infi],
id                    └────────────────┘
src      └─────────┘ └┘└────────────────┘
typ      └─────────┘└┘└────────────────┘
doc      └─────────┘ └┘                  
txt      └─────────┘ └┘                  
par      └─────────┘ └┘                  
pid          └──┘└┘ └┘                  
st   ────────────────────────────────────┘└─
100      exact is_measurable.bInter (countable_encodable _) (assume i _, he₁ _) },
id             └──────────────────┘  └─────────────────┘                 └─┘
src      └────┘└──────────────────┘ └─────────────────┘└──┘       └────┘   └──┘
typ      └────┘└──────────────────┘ └─────────────────┘└──┘       └────┘└─┘└──┘
doc      └────┘                                        └──┘       └────┘   └──┘
txt      └────┘                                        └──┘       └────┘   └──┘
par      └────┘                                        └──┘       └────┘   └──┘
pid                                                   └──┘       └────┘   └─┘
st   ──────────────────────────────────────────────────────────────────────────┘└┘
101  
st   
102    have f_subset_f : ∀{a b c d}, a ≤ b → c ≤ d → f a d ⊆ f b c,
id                                                         
src    └────────────────┘ └───────┘               
typ    └────────────────┘ └───────┘            
doc    └────────────────┘ └───────┘               
txt    └────────────────┘ └───────┘               
par    └────────────────┘ └───────┘               
pid    └─────────────┘└─┘ └───────┘               
st   ────────────────────────────────────────────────────────────┘└─
103    { assume a b c d hab hcd,
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid      └────────────────────┘
st   ───┘└────────────────────┘└─
104      dsimp only [f],
id                   
src      └──────────┘ 
typ      └──────────┘
doc      └──────────┘ 
txt      └──────────┘ 
par      └──────────┘ 
pid           └───┘└┘ 
st   ─────────────────┘└─
105      rw [finset.inf_eq_infi, finset.inf_eq_infi],
id           └────────────────┘  └────────────────┘
src      └──┘└────────────────┘└┘└────────────────┘
typ      └──┘└────────────────┘└┘└────────────────┘
doc      └──┘                  └┘                  
txt      └──┘                  └┘                  
par      └──┘                  └┘                  
pid        └┘                  └┘                  
st   ─────────────────────────┘└──────────────────┘└──
106      refine bInter_subset_bInter_left _,
id              └───────────────────────┘
src      └─────┘└───────────────────────┘└┘
typ      └─────┘└───────────────────────┘└┘
doc      └─────┘                         └┘
txt      └─────┘                         └┘
par      └─────┘                         └┘
pid                                     └┘
st   ─────────────────────────────────────┘└─
107      simp,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
108      rintros j ⟨hbj, hjc⟩,
src      └──────────────────┘
typ      └──────────────────┘
doc      └──────────────────┘
txt      └──────────────────┘
par      └──────────────────┘
pid             └───────────┘
st   ───────────────────────┘└─
109      exact ⟨le_trans hab hbj, lt_of_lt_of_le hjc $ add_le_add_right hcd 1⟩ },
id              └──────┘ └─┘ └─┘  └────────────┘ └─┘   └──────────────┘ └─┘
src      └────┘ └──────┘      └┘└────────────┘    └──────────────┘   └──┘
typ      └────┘ └──────┘└─┘└─┘└┘└────────────┘└─┘ └──────────────┘└─┘└──┘
doc      └────┘               └┘                                     └──┘
txt      └────┘               └┘                                     └──┘
par      └────┘               └┘                                     └──┘
pid                          └┘                                     └─┘
st   ─────────────────────────────────────────────────────────────────────────┘└┘
110  
st   
111    have f_succ : ∀n m, n ≤ m → f n (m + 1) = f n m ∩ e (m + 1),
id                                                      
src    └────────────┘ └─┘          └──┘         └─┘
typ    └────────────┘ └─┘          └──┘       └─┘
doc    └────────────┘ └─┘          └──┘         └─┘
txt    └────────────┘ └─┘          └──┘         └─┘
par    └────────────┘ └─┘          └──┘         └─┘
pid    └─────────┘└─┘ └─┘          └──┘         └─┘
st   ────────────────────────────────────────────────────────────┘└─
112    { assume n m hnm,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid      └────────────┘
st   ───┘└────────────┘└─
113      have : n ≤ m + 1 := le_of_lt (nat.succ_le_succ hnm),
id                         └──────┘  └──────────────┘ └─┘
src      └─────┘    └────┘└──────┘ └──────────────┘   
typ      └─────┘  └────┘└──────┘ └──────────────┘└─┘
doc      └─────┘    └────┘                            
txt      └─────┘    └────┘                            
par      └─────┘    └────┘                            
pid      └───┘└┘    └───┘                            
st   ──────────────────────────────────────────────────────┘└─
114      simp only [f],
id                  
src      └─────────┘ 
typ      └─────────┘
doc      └─────────┘ 
txt      └─────────┘ 
par      └─────────┘ 
pid          └──┘└┘ 
st   ────────────────┘└─
115      rw [finset.Ico.succ_top this, finset.inf_insert, set.inter_comm],
id           └─────────────────┘ └──┘  └───────────────┘  └────────────┘
src      └──┘└─────────────────┘    └┘└───────────────┘└┘└────────────┘
typ      └──┘└─────────────────┘└──┘└┘└───────────────┘└┘└────────────┘
doc      └──┘                       └┘                 └┘              
txt      └──┘                       └┘                 └┘              
par      └──┘                       └┘                 └┘              
pid        └┘                       └┘                 └┘              
st   ───────────────────────────────┘└─────────────────┘└──────────────┘└──
116      refl },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ────────┘└┘
117  
st   
118    have le_d_f : ∀n m, m ≤ n → γ - 2 * ((1 / 2) ^ m) + (1 / 2) ^ n ≤ d (f m n),
id                                                                      
src    └────────────┘ └─┘       └─┘  └┘ └──┘  └┘  └┘ └──┘        
typ    └────────────┘ └─┘     └─┘  └┘ └──┘  └┘  └┘ └──┘      
doc    └────────────┘ └─┘       └─┘   └┘ └──┘  └┘  └┘ └──┘        
txt    └────────────┘ └─┘       └─┘   └┘ └──┘  └┘  └┘ └──┘        
par    └────────────┘ └─┘       └─┘   └┘ └──┘  └┘  └┘ └──┘        
pid    └─────────┘└─┘ └─┘       └─┘   └┘ └──┘  └┘  └┘ └──┘        
st   ────────────────────────────────────────────────────────────────────────────┘└─
119    { assume n m h,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid      └──────────┘
st   ───┘└──────────┘└─
120      refine nat.le_induction _ _ n h,
id              └──────────────┘      
src      └─────┘└──────────────┘└───┘ 
typ      └─────┘└──────────────┘└───┘
doc      └─────┘└──────────────┘└───┘ 
txt      └─────┘                └───┘ 
par      └─────┘                └───┘ 
pid                            └───┘ 
st   ──────────────────────────────────┘└─
121      { have := he₂ m,
id                 └─┘ 
src        └──────┘   
typ        └──────┘└─┘
doc        └──────┘   
txt        └──────┘   
par        └──────┘   
pid        └───┘└─┘   
st   ─────┘└───────────┘└─
122        simp only [f],
id                    
src        └─────────┘ 
typ        └─────────┘
doc        └─────────┘ 
txt        └─────────┘ 
par        └─────────┘ 
pid            └──┘└┘ 
st   ──────────────────┘└─
123        rw [finset.Ico.succ_singleton, finset.inf_singleton],
id             └───────────────────────┘  └──────────────────┘
src        └──┘└───────────────────────┘└┘└──────────────────┘
typ        └──┘└───────────────────────┘└┘└──────────────────┘
doc        └──┘                         └┘                    
txt        └──┘                         └┘                    
par        └──┘                         └┘                    
pid          └┘                         └┘                    
st   ──────────────────────────────────┘└────────────────────┘└──
124        exact aux this },
id               └─┘ └──┘
src        └────┘└─┘    
typ        └────┘└─┘└──┘
doc        └────┘       
txt        └────┘       
par        └────┘       
pid                    
st   ────────────────────┘└┘
125      { assume n (hmn : m ≤ n) ih,
id                            
src        └──────────────┘   └──┘
typ        └──────────────┘ └──┘
doc        └──────────────┘   └──┘
txt        └──────────────┘   └──┘
par        └──────────────┘   └──┘
pid        └──────────────┘   └──┘
st   ──────────────────────────────┘└─
126        have : γ + (γ - 2 * (1 / 2)^m + (1 / 2) ^ (n + 1)) ≤ γ + d (f m (n + 1)),
id                                                                      
src        └─────┘     └─┘  └┘ └─┘    └┘ └──┘    └───┘          └──┘
typ        └─────┘     └─┘  └┘ └─┘    └┘ └──┘    └───┘     └──┘
doc        └─────┘     └─┘  └┘ └─┘    └┘ └──┘    └───┘          └──┘
txt        └─────┘     └─┘  └┘ └─┘    └┘ └──┘    └───┘          └──┘
par        └─────┘     └─┘  └┘ └─┘    └┘ └──┘    └───┘          └──┘
pid        └───┘└┘     └─┘  └┘ └─┘    └┘ └──┘    └───┘          └──┘
st   ─────────────────────────────────────────────────────────────────────────────┘└─
127        { calc γ + (γ - 2 * (1 / 2)^m + (1 / 2) ^ (n+1)) ≤
id           └──┘
src          └──┘
typ          └──┘
doc          └──┘
st   ───────┘└────────────────────────────────────────────────
128              γ + (γ - 2 * (1 / 2)^m + ((1 / 2) ^ n - (1/2)^(n+1))) :
id                                                            
typ                                                           
st   ────────────────────────────────────────────────────────────────────
129            begin
st   ─────────┘└─────
130              refine add_le_add_left (add_le_add_left _ _) γ,
id                                       └─────────────┘      
src              └─────┘                └─────────────┘└────┘
typ              └─────┘                └─────────────┘└────┘
doc              └─────┘                               └────┘
txt              └─────┘                               └────┘
par              └─────┘                               └────┘
pid                                                   └────┘
st   ─────────────────────────────────────────────────────────┘└─
131              simp only [pow_add, pow_one, le_sub_iff_add_le],
id                          └─────┘  └─────┘  └───────────────┘
src              └─────────┘└─────┘└┘└─────┘└┘└───────────────┘
typ              └─────────┘└─────┘└┘└─────┘└┘└───────────────┘
doc              └─────────┘       └┘       └┘                 
txt              └─────────┘       └┘       └┘                 
par              └─────────┘       └┘       └┘                 
pid                  └──┘└┘       └┘       └┘                 
st   ──────────────────────────────────────────────────────────┘└─
132              linarith
src              └────────
typ              └────────
doc              └────────
txt              └────────
par              └────────
pid                      
st   ─────────────────────
133            end
src  ─────────┘
typ  ─────────┘
doc  ─────────┘
txt  ─────────┘
par  ─────────┘
pid  ─────────┘
st   ─────────┘└─┘
134            ... = (γ - (1 / 2)^(n+1)) + (γ - 2 * (1 / 2)^m + (1 / 2)^n) :
st   ────────────────────────────────────────────────────────────────────────
135              by simp only [sub_eq_add_neg]; ac_refl
id                             └────────────┘
src                 └─────────┘└────────────┘  └───────
typ                 └─────────┘└────────────┘  └───────
doc                 └─────────┘                └───────
txt                 └─────────┘                └───────
par                 └─────────┘                └───────
pid                     └──┘└┘                       
st   ─────────────┘└────────────────────────────────────
136            ... ≤ d (e (n + 1)) + d (f m n) : add_le_add (le_of_lt $ he₂ _) ih
id                                            └────────┘  └──────┘   └─┘    └┘
src  ─────────┘                                  └────────┘  └──────┘
typ  ─────────┘                               └────────┘  └──────┘   └─┘    └┘
doc  ─────────┘
txt  ─────────┘
par  ─────────┘
pid  ─────────┘
st   ─────────┘└──────────────────────────────────────────────────────────────────
137            ... ≤ d (e (n + 1)) + d (f m n \ e (n + 1)) + d (f m (n + 1)) :
st   ──────────────────────────────────────────────────────────────────────────
138              by rw [f_succ _ _ hmn, d_split (f m n) (e (n + 1)) (hf _ _) (he₁ _), add_assoc]
id                      └────┘     └─┘  └─────┘                  └┘       └─┘     └───────┘
src                 └──┘      └───┘   └┘           └┘     └───┘   └────┘    └───┘└───────┘└─
typ                 └──┘└────┘└───┘└─┘└┘└─────┘  └┘   └───┘ └┘└────┘ └─┘└───┘└───────┘└─
doc                 └──┘      └───┘   └┘           └┘     └───┘   └────┘    └───┘         └─
txt                 └──┘      └───┘   └┘           └┘     └───┘   └────┘    └───┘         └─
par                 └──┘      └───┘   └┘           └┘     └───┘   └────┘    └───┘         └─
pid                   └┘      └───┘   └┘           └┘     └───┘   └────┘    └───┘         
st   ─────────────┘└─────────────────┘└────────────────────────────────────────────┘└─────────┘
139            ... = d (e (n + 1) ∪ f m n) + d (f m (n + 1)) :
id                                
src  ─────────┘                   
typ  ─────────┘                   
doc  ─────────┘
txt  ─────────┘
par  ─────────┘
pid  ─────────┘
st   ─────────┘└───────────────────────────────────────────────
140              begin
st   ───────────┘└─────
141                rw [d_split (e (n + 1) ∪ f m n) (e (n + 1)),
id                     └─────┘                      
src                └──┘            └──┘    └┘     └─────
typ                └──┘└─────┘     └──┘  └┘   └─────
doc                └──┘            └──┘    └┘     └─────
txt                └──┘            └──┘    └┘     └─────
par                └──┘            └──┘    └┘     └─────
pid                  └┘            └──┘    └┘     └─────
st   ────────────────────────────────────────────────────────┘└─
142                  union_diff_left, union_inter_cancel_left],
id                   └─────────────┘  └─────────────────────┘
src  ───────────────┘└─────────────┘└┘└─────────────────────┘
typ  ───────────────┘└─────────────┘└┘└─────────────────────┘
doc  ───────────────┘               └┘                       
txt  ───────────────┘               └┘                       
par  ───────────────┘               └┘                       
pid  ───────────────┘               └┘                       
st   ──────────────────────────────┘└───────────────────────┘└──
143                ac_refl,
src                └─────┘
typ                └─────┘
doc                └─────┘
txt                └─────┘
par                └─────┘
st   ────────────────────┘└─
144                exact (he₁ _).union (hf _ _),
id                        └─┘           └┘
src                └────┘    └────────┘   └───┘
typ                └────┘ └─┘└────────┘ └┘└───┘
doc                └────┘    └────────┘   └───┘
txt                └────┘    └────────┘   └───┘
par                └────┘    └────────┘   └───┘
pid                         └────────┘   └───┘
st   ─────────────────────────────────────────┘└─
145                exact (he₁ _)
id                        └─┘
src                └────┘    └───
typ                └────┘ └─┘└───
doc                └────┘    └───
txt                └────┘    └───
par                └────┘    └───
pid                         └─┘
st   ────────────────────────────
146              end
src  ───────────┘
typ  ───────────┘
doc  ───────────┘
txt  ───────────┘
par  ───────────┘
pid  ───────────┘
st   ───────────┘└─┘
147            ... ≤ γ + d (f m (n + 1)) :
st   ──────────────────────────────────────
148              add_le_add_right (d_le_γ _ $ (he₁ _).union (hf _ _)) _ },
id               └──────────────┘  └────┘            └───┘
src              └──────────────┘                    └───┘
typ              └──────────────┘  └────┘            └───┘
st   ─────────────────────────────────────────────────────────────────┘└─┘
149        exact (add_le_add_iff_left γ).1 this } },
id                └─────────────────┘     └──┘
src        └────┘ └─────────────────┘ └──┘    
typ        └────┘ └─────────────────┘└──┘└──┘
doc        └────┘                     └──┘    
txt        └────┘                     └──┘    
par        └────┘                     └──┘    
pid                                  └──┘    
st   ──────────────────────────────────────────┘└──┘
150  
st   
151    let s := ⋃ m, ⋂n, f m n,
id                   
src    └───────┘└┘  
typ    └───────┘└┘ 
doc    └───────┘└┘  
txt    └───────┘ └┘     
par    └───────┘ └┘     
pid    └───┘└─┘ └┘     
st   ────────────────────────┘└─
152    have γ_le_d_s : γ ≤ d s,
id                         
src    └──────────────┘   
typ    └──────────────┘ 
doc    └──────────────┘   
txt    └──────────────┘   
par    └──────────────┘   
pid    └───────────┘└─┘   
st   ────────────────────────┘└─
153    { have hγ : tendsto (λm:ℕ, γ - 2 * (1/2)^m) at_top (𝓝 γ),
id                 └─────┘                         └────┘    
src      └────────┘└─────┘  └┘ └┘  └─┘   └┘  └┘└────┘   
typ      └────────┘└─────┘  └┘ └┘  └─┘   └┘  └┘└────┘  
doc      └────────┘└─────┘  └┘ └┘  └─┘   └┘  └┘└────┘   
txt      └────────┘         └┘ └┘  └─┘   └┘  └┘         
par      └────────┘         └┘ └┘  └─┘   └┘  └┘         
pid      └─────┘└─┘         └┘ └┘  └─┘   └┘  └┘         
st   ───┘└────────────────────────────────────────────────────┘└─
154      { suffices : tendsto (λm:ℕ, γ - 2 * (1/2)^m) at_top (𝓝 (γ - 2 * 0)), { simpa },
id                    └─────┘                         └────┘     
src        └─────────┘└─────┘  └┘ └┘  └─┘   └┘  └┘└────┘     └─┘ └──┘    └────┘
typ        └─────────┘└─────┘  └┘ └┘  └─┘   └┘  └┘└────┘    └─┘ └──┘    └────┘
doc        └─────────┘└─────┘  └┘ └┘  └─┘   └┘  └┘└────┘     └─┘ └──┘    └────┘
txt        └─────────┘         └┘ └┘  └─┘   └┘  └┘           └─┘ └──┘    └────┘
par        └─────────┘         └┘ └┘  └─┘   └┘  └┘           └─┘ └──┘    └────┘
pid        └───────┘└┘         └┘ └┘  └─┘   └┘  └┘           └─┘ └──┘         
st   ─────┘└───────────────────────────────────────────────────────────────┘└──┘└────┘└┘
155        exact (tendsto_const_nhds.sub $ tendsto_const_nhds.mul $
id                └────────────────────┘   └────────────────────┘
src        └────┘ └────────────────────┘ └────────────────────┘ 
typ        └────┘ └────────────────────┘ └────────────────────┘ 
doc        └────┘                                               
txt        └────┘                                               
par        └────┘                                               
pid                                                            
st   ───────────────────────────────────────────────────────────────
156          tendsto_pow_at_top_nhds_0_of_lt_1
id           └───────────────────────────────┘
src  ───────┘└───────────────────────────────┘
typ  ───────┘└───────────────────────────────┘
doc  ───────┘                                 
txt  ───────┘                                 
par  ───────┘                                 
pid  ───────┘                                 
st   ──────────────────────────────────────────
157            (le_of_lt $ half_pos $ zero_lt_one) (half_lt_self zero_lt_one)) },
id              └──────┘   └──────┘                 └──────────┘ └─────────┘
src  ─────────┘ └──────┘ └──────┘            └┘ └──────────┘└─────────┘└─┘
typ  ─────────┘ └──────┘ └──────┘            └┘ └──────────┘└─────────┘└─┘
doc  ─────────┘                              └┘                        └─┘
txt  ─────────┘                              └┘                        └─┘
par  ─────────┘                              └┘                        └─┘
pid  ─────────┘                              └┘                        └┘
st   ─────────────────────────────────────────────────────────────────────────┘└┘
158      have hd : tendsto (λm, d (⋂n, f m n)) at_top (𝓝 (d (⋃ m, ⋂ n, f m n))),
id                 └─────┘                     └────┘             
src      └────────┘└─────┘  └─┘       └─┘└────┘     └┘└┘   └─┘
typ      └────────┘└─────┘  └─┘       └─┘└────┘    └┘└┘  └─┘
doc      └────────┘└─────┘  └─┘       └─┘└────┘     └┘└┘   └─┘
txt      └────────┘         └─┘       └─┘            └┘  └┘    └─┘
par      └────────┘         └─┘       └─┘            └┘  └┘    └─┘
pid      └─────┘└─┘         └─┘       └─┘            └┘  └┘    └─┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
159      { refine d_Union _ _ _,
id                └─────┘
src        └─────┘       └────┘
typ        └─────┘└─────┘└────┘
doc        └─────┘       └────┘
txt        └─────┘       └────┘
par        └─────┘       └────┘
pid                     └────┘
st   ─────┘└──────────────────┘└─
160        { assume n, exact is_measurable.Inter (assume m, hf _ _) },
id                           └─────────────────┘            └┘
src          └──────┘  └────┘└─────────────────┘       └──┘  └────┘
typ          └──────┘  └────┘└─────────────────┘       └──┘└┘└────┘
doc          └──────┘  └────┘                          └──┘  └────┘
txt          └──────┘  └────┘                          └──┘  └────┘
par          └──────┘  └────┘                          └──┘  └────┘
pid          └──────┘                                 └──┘  └───┘
st   ───────┘└──────┘└─────────────────────────────────────────────┘└┘
161        { exact assume n m hnm, subset_Inter
id                                 └──────────┘
src          └────┘      └────────┘└──────────┘
typ          └────┘      └────────┘└──────────┘
doc          └────┘      └────────┘            
txt          └────┘      └────────┘            
par          └────┘      └────────┘            
pid                     └────────┘            
st   ───────────────────────────────────────────
162            (assume i, subset.trans (Inter_subset (f n) i) $ f_subset_f hnm $ le_refl _) } },
id                        └──────────┘  └──────────┘           └────────┘       └─────┘
src  ─────────┘       └──┘└──────────┘ └──────────┘   └┘ └┘               └─────┘└──┘
typ  ─────────┘       └──┘└──────────┘ └──────────┘  └┘ └┘ └────────┘    └─────┘└──┘
doc  ─────────┘       └──┘                            └┘ └┘                      └──┘
txt  ─────────┘       └──┘                            └┘ └┘                      └──┘
par  ─────────┘       └──┘                            └┘ └┘                      └──┘
pid  ─────────┘       └──┘                            └┘ └┘                      └─┘
st   ──────────────────────────────────────────────────────────────────────────────────────┘└──┘
163      refine le_of_tendsto_of_tendsto (@at_top_ne_bot ℕ _ _) hγ hd (univ_mem_sets' $ assume m, _),
id              └──────────────────────┘   └───────────┘        └┘ └┘  └────────────┘
src      └─────┘└──────────────────────┘  └───────────┘ └────┘     └────────────┘       └────┘
typ      └─────┘└──────────────────────┘  └───────────┘ └────┘└┘└┘ └────────────┘       └────┘
doc      └─────┘                                        └────┘                          └────┘
txt      └─────┘                                        └────┘                          └────┘
par      └─────┘                                        └────┘                          └────┘
pid                                                    └────┘                          └────┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
164      change γ - 2 * (1 / 2) ^ m ≤ d (⋂ (n : ℕ), f m n),
id                                               
src      └─────┘  └─┘  └┘ └──┘     └────┘    
typ      └─────┘ └─┘  └┘ └──┘    └────┘  
doc      └─────┘  └─┘  └┘ └──┘     └────┘    
txt      └─────┘  └─┘  └┘ └──┘      └────┘     
par      └─────┘  └─┘  └┘ └──┘      └────┘     
pid              └─┘  └┘ └──┘      └────┘     
st   ────────────────────────────────────────────────────┘└─
165      have : tendsto (λn, d (f m n)) at_top (𝓝 (d (⋂ n, f m n))),
id              └─────┘                 └────┘           
src      └─────┘└─────┘  └─┘     └─┘└────┘     └┘   └─┘
typ      └─────┘└─────┘  └─┘     └─┘└────┘    └┘ └─┘
doc      └─────┘└─────┘  └─┘     └─┘└────┘     └┘   └─┘
txt      └─────┘         └─┘     └─┘            └┘    └─┘
par      └─────┘         └─┘     └─┘            └┘    └─┘
pid      └───┘└┘         └─┘     └─┘            └┘    └─┘
st   ─────────────────────────────────────────────────────────────┘└─
166      { refine d_Inter _ _ _,
id                └─────┘
src        └─────┘       └────┘
typ        └─────┘└─────┘└────┘
doc        └─────┘       └────┘
txt        └─────┘       └────┘
par        └─────┘       └────┘
pid                     └────┘
st   ─────┘└──────────────────┘└─
167        { assume n, exact hf _ _ },
id                           └┘
src          └──────┘  └────┘  └───┘
typ          └──────┘  └────┘└┘└───┘
doc          └──────┘  └────┘  └───┘
txt          └──────┘  └────┘  └───┘
par          └──────┘  └────┘  └───┘
pid          └──────┘         └──┘
st   ───────┘└──────┘└─────────────┘└┘
168        { assume n m hnm, exact f_subset_f (le_refl _) hnm } },
id                                 └────────┘  └─────┘    └─┘
src          └────────────┘  └────┘           └─────┘└──┘   
typ          └────────────┘  └────┘└────────┘ └─────┘└──┘└─┘
doc          └────────────┘  └────┘                  └──┘   
txt          └────────────┘  └────┘                  └──┘   
par          └────────────┘  └────┘                  └──┘   
pid          └────────────┘                         └──┘   
st   ─────────────────────┘└─────────────────────────────────┘└──┘
169      refine ge_of_tendsto (@at_top_ne_bot ℕ _ _) this (mem_at_top_sets.2 ⟨m, assume n hmn, _⟩),
id              └───────────┘   └───────────┘        └──┘  └─────────────┘    
src      └─────┘└───────────┘  └───────────┘ └────┘     └─────────────┘└─┘  └┘      └─────────┘
typ      └─────┘└───────────┘  └───────────┘ └────┘└──┘ └─────────────┘└─┘ └┘      └─────────┘
doc      └─────┘                             └────┘                    └─┘  └┘      └─────────┘
txt      └─────┘                             └────┘                    └─┘  └┘      └─────────┘
par      └─────┘                             └────┘                    └─┘  └┘      └─────────┘
pid                                         └────┘                    └─┘  └┘      └─────────┘
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─
170      change γ - 2 * (1 / 2) ^ m ≤ d (f m n),
id                                       
src      └─────┘  └─┘  └┘ └──┘        
typ      └─────┘ └─┘  └┘ └──┘    
doc      └─────┘  └─┘  └┘ └──┘        
txt      └─────┘  └─┘  └┘ └──┘        
par      └─────┘  └─┘  └┘ └──┘        
pid              └─┘  └┘ └──┘        
st   ─────────────────────────────────────────┘└─
171      refine le_trans _ (le_d_f _ _ hmn),
id              └──────┘    └────┘     └─┘
src      └─────┘└──────┘└─┘       └───┘   
typ      └─────┘└──────┘└─┘ └────┘└───┘└─┘
doc      └─────┘        └─┘       └───┘   
txt      └─────┘        └─┘       └───┘   
par      └─────┘        └─┘       └───┘   
pid                    └─┘       └───┘   
st   ─────────────────────────────────────┘└─
172      exact le_add_of_le_of_nonneg (le_refl _) (pow_nonneg (le_of_lt $ half_pos $ zero_lt_one) _) },
id             └────────────────────┘  └─────┘     └────────┘  └──────┘   └──────┘   └─────────┘
src      └────┘└────────────────────┘ └─────┘└──┘ └────────┘ └──────┘ └──────┘ └─────────┘└───┘
typ      └────┘└────────────────────┘ └─────┘└──┘ └────────┘ └──────┘ └──────┘ └─────────┘└───┘
doc      └────┘                              └──┘                                         └───┘
txt      └────┘                              └──┘                                         └───┘
par      └────┘                              └──┘                                         └───┘
pid                                         └──┘                                         └──┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└┘
173  
st   
174    have hs : is_measurable s :=
id               └───────────┘ 
src    └────────┘└───────────┘ └───
typ    └────────┘└───────────┘└───
doc    └────────┘└───────────┘ └───
txt    └────────┘              └───
par    └────────┘              └───
pid    └─────┘└─┘              └───
st   ───────────────────────────────
175      is_measurable.Union (assume n, is_measurable.Inter (assume m, hf _ _)),
id       └─────────────────┘            └─────────────────┘            └┘
src  ───┘└─────────────────┘       └──┘└─────────────────┘       └──┘  └────┘
typ  ───┘└─────────────────┘       └──┘└─────────────────┘       └──┘└┘└────┘
doc  ───┘                          └──┘                          └──┘  └────┘
txt  ───┘                          └──┘                          └──┘  └────┘
par  ───┘                          └──┘                          └──┘  └────┘
pid  ───┘                          └──┘                          └──┘  └────┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
176    refine ⟨s, hs, _, _⟩,
id               └┘
src    └─────┘  └┘  └─────┘
typ    └─────┘ └┘└┘└─────┘
doc    └─────┘  └┘  └─────┘
txt    └─────┘  └┘  └─────┘
par    └─────┘  └┘  └─────┘
pid            └┘  └─────┘
st   ─────────────────────┘└─
177    { assume t ht hts,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid      └─────────────┘
st   ───┘└─────────────┘└─
178      have : 0 ≤ d t := ((add_le_add_iff_left γ).1 $
id                         └─────────────────┘
src      └───────┘   └──┘  └─────────────────┘ └──┘ 
typ      └───────┘ └──┘  └─────────────────┘ └──┘ 
doc      └───────┘   └──┘                      └──┘ 
txt      └───────┘   └──┘                      └──┘ 
par      └───────┘   └──┘                      └──┘ 
pid      └───┘└──┘   └──┘                      └──┘ 
st   ───────────────────────────────────────────────────
179        calc γ + 0 ≤ d s : by rw [add_zero]; exact γ_le_d_s
id                                 └──────┘         └──────┘
src  ─────┘      └─┘   └─┘  └──┘└──────┘└┘└────┘        
typ  ─────┘      └─┘ └─┘  └──┘└──────┘└┘└────┘└──────┘
doc  ─────┘      └─┘   └─┘  └──┘        └┘└────┘        
txt  ─────┘      └─┘   └─┘  └──┘        └┘└────┘        
par  ─────┘      └─┘   └─┘  └──┘        └┘└────┘        
pid  ─────┘      └─┘   └─┘  └───┘        └───────┘        
st   ──────────────────────────┘└───────────┘└────────────────
180          ... = d (s \ t) + d t : by rw [d_split _ _ hs ht, inter_eq_self_of_subset_right hts]
id                                          └─────┘     └┘ └┘  └───────────────────────────┘ └─┘
src  ───────┘└──┘      └┘   └─┘  └──┘       └───┘    └┘└───────────────────────────┘   └─
typ  ───────┘└──┘      └┘   └─┘  └──┘└─────┘└───┘└┘└┘└┘└───────────────────────────┘└─┘└─
doc  ───────┘└──┘      └┘   └─┘  └──┘       └───┘    └┘                                └─
txt  ───────┘└──┘      └┘   └─┘  └──┘       └───┘    └┘                                └─
par  ───────┘└──┘      └┘   └─┘  └──┘       └───┘    └┘                                └─
pid  ───────────┘      └┘   └─┘  └───┘       └───┘    └┘                                └─
st   ───────┘└────────────────────────┘└────────────────────┘└─────────────────────────────────┘
181          ... ≤ γ + d t : add_le_add (d_le_γ _ (hs.diff ht)) (le_refl _)),
id                         └────────┘  └────┘    └─────┘ └┘    └─────┘
src  ───────┘└──┘     └─┘└────────┘       └─┘ └─────┘  └─┘ └─────┘└──┘
typ  ───────┘└──┘   └─┘└────────┘ └────┘└─┘ └─────┘└┘└─┘ └─────┘└──┘
doc  ───────┘└──┘     └─┘                 └─┘          └─┘        └──┘
txt  ───────┘└──┘     └─┘                 └─┘          └─┘        └──┘
par  ───────┘└──┘     └─┘                 └─┘          └─┘        └──┘
pid  ───────────┘     └─┘                 └─┘          └─┘        └──┘
st   ───────┘└─────────────────────────────────────────────────────────────┘└─
182      rw [← to_nnreal_μ, ← to_nnreal_ν, ennreal.coe_le_coe, ← nnreal.coe_le],
id             └─────────┘    └─────────┘  └────────────────┘    └───────────┘
src      └────┘           └──┘           └┘└────────────────┘└──┘└───────────┘
typ      └────┘└─────────┘└──┘└─────────┘└┘└────────────────┘└──┘└───────────┘
doc      └────┘           └──┘           └┘                  └──┘             
txt      └────┘           └──┘           └┘                  └──┘             
par      └────┘           └──┘           └┘                  └──┘             
pid        └──┘           └──┘           └┘                  └──┘             
st   ────────────────────┘└─────────────┘└──────────────────┘└───────────────┘└──
183      simpa only [d, le_sub_iff_add_le, zero_add] using this },
id                     └───────────────┘  └──────┘        └──┘
src      └──────────┘ └┘└───────────────┘└┘└──────┘└──────┘    
typ      └──────────┘└┘└───────────────┘└┘└──────┘└──────┘└──┘
doc      └──────────┘ └┘                 └┘        └──────┘    
txt      └──────────┘ └┘                 └┘        └──────┘    
par      └──────────┘ └┘                 └┘        └──────┘    
pid           └──┘└┘ └┘                 └┘        └────┘    
st   ──────────────────────────────────────────────────────────┘
184    { assume t ht hts,
185      have : d t ≤ 0,
id               
typ              
186      exact ((add_le_add_iff_left γ).1 $
187        calc γ + d t ≤ d s + d t : add_le_add γ_le_d_s (le_refl _)
id                                              └┘  └┘
typ                                             └┘  └┘
188          ... = d (s ∪ t) :
189          begin
190            rw [d_split _ _ (hs.union ht) ht, union_diff_right, union_inter_cancel_right,
191              diff_eq_self.2],
192            exact assume a ⟨hat, has⟩, hts hat has
id                          
typ                         
193          end
st           └─┘
194          ... ≤ γ + 0 : by rw [add_zero]; exact d_le_γ _ (hs.union ht)),
id                                                                   └┘
typ                                                                  └┘
195      rw [← to_nnreal_μ, ← to_nnreal_ν, ennreal.coe_le_coe, ← nnreal.coe_le],
196      simpa only [d, sub_le_iff_le_add, zero_add] using this }
id                   
typ                  
st                                                              └─
197  end
st   ──┘
198  
199  end measure_theory